module sva_ca_sequence;

    logic clk;
    initial begin
        clk = 0;
        forever #5 clk = ~clk;
    end

    logic a, b, c, d;
    initial begin
        a = 1; b = 0; c = 1; d = 1; #5;
        a = 1; b = 1; c = 1; d = 1; #10;
        a = 0; b = 0; c = 1; d = 1; #10;
        a = 0; b = 1; c = 1; d = 0; #10;
        a = 0; b = 1; c = 1; d = 1; #10;
        a = 0; b = 1; c = 1; d = 1; #10;
        $finish;
    end

    sequence seq1;
        a ##1 b ##1 c;
    endsequence

    sequence seq2;
        a ##1 d;
    endsequence

    sequence seq3;
        c ##2 d;
    endsequence

    sequence seq1_and_seq2;
        // and 逻辑与: 两个序列必须同时匹配
        // 两序列从相同起始点开始, 结束时间可以不同, 整体序列在最后结束的子序列完成时匹配.
        seq1 and seq2;
    endsequence

    sequence seq1_or_seq2;
        // or 逻辑或: 任一序列匹配即可
        // 任一子序列匹配即视为整体匹配
        // 每一个操作数序列的成功匹配都会构成复合序列的一个成功匹配, 并且结束时间与原操作数序列的结束时间相同
        seq1 or seq2;
    endsequence

    sequence seq1_intersect_seq3;
        // intersect 时序交:
        // 两序列须同时开始且同时结束, 即两个操作数序列的匹配长度必须完全相同, 两个操作数序列都必须匹配成功.
        seq1 intersect seq3;
    endsequence

    sequence seq_first_match;
        // first_match 首次匹配:
        // 如果操作数序列没有匹配, 则 first_match 也没有匹配;
        // 如果操作数序列有多个匹配, first_match 只会匹配那个结束时间最早的匹配;
        // 如果存在多个结束时间同为最早的匹配, 那么所有这些匹配都会被认为是 first_match 的匹配.
        // 下例中, 序列存在 4 种情况: a ##2 b / a ##3 b / c ##1 d / c ##2 d
        first_match((a ##[2:3] b) or (c ##[1:2] d));
    endsequence

    property prty_seq1_and_seq2;
        @(posedge clk) a |-> seq1_and_seq2;
    endproperty
    cap1: assert property (prty_seq1_and_seq2) $info("cap1 passed"); else $error("cap1 failed");

    property prty_seq1_or_seq2;
        @(posedge clk) a |-> seq1_or_seq2;
    endproperty
    cap2: assert property (prty_seq1_or_seq2) $info("cap2 passed"); else $error("cap2 failed");

    property prty_seq1_intersect_seq3;
        @(posedge clk) a |-> seq1_intersect_seq3;
    endproperty
    cap3: assert property (prty_seq1_intersect_seq3) $info("cap3 passed"); else $error("cap3 failed");

    property prty_seq_first_match;
        @(posedge clk) a |-> seq_first_match;
    endproperty
    cap4: assert property (prty_seq_first_match) $info("cap4 passed"); else $error("cap4 failed");

    // throughout 操作符 等价于 (expr) [*0:$] intersect seq
    /*  property burst_rule;
            $fell(burst_mode) |->                   // 触发条件
                (!burst_mode) throughout            // 持续条件
                    (##2 (trdy==0 && irdy==0)[*7]); // 核心事件序列
        endproperty
        上述代码含义:
        $fell(burst_mode) 检测 burst_mode 的下降沿, 标志突发传输开始.
        (!burst_mode) throughout seq 要求整个事件序列持续期间 burst_mode 保持低电平, 其等价于 (!burst_mode) [*0:$] intersect seq
        ##2 (trdy==0 && irdy==0)[*7] 要求 2 个时钟周期后, (trdy==0)&&(irdy==0) 必须连续保持7个时钟周期为真
     */

    // seq.ended 用于检测序列在当前时钟周期是否完成匹配
    property prty_seq_ended;
        @(posedge clk) seq1.ended |-> seq3.ended;
    endproperty
    cap5: assert property (prty_seq_ended) $info("cap5 passed"); else $error("cap5 failed");

    initial begin
        $dumpfile("dump.vcd"); $dumpvars;
    end
endmodule

/* Output: QuestaSim
# ** Info: cap4 passed
#    Time: 15 ns Started: 5 ns  Scope: sva_ca_sequence.cap4 File: sva_ca_sequence.sv Line: 78
# ** Info: cap2 passed
#    Time: 15 ns Started: 5 ns  Scope: sva_ca_sequence.cap2 File: sva_ca_sequence.sv Line: 68
# ** Error: cap3 failed
#    Time: 25 ns Started: 15 ns  Scope: sva_ca_sequence.cap3 File: sva_ca_sequence.sv Line: 73
# ** Info: cap3 passed
#    Time: 25 ns Started: 5 ns  Scope: sva_ca_sequence.cap3 File: sva_ca_sequence.sv Line: 73
# ** Info: cap4 passed
#    Time: 25 ns Started: 15 ns  Scope: sva_ca_sequence.cap4 File: sva_ca_sequence.sv Line: 78
# ** Info: cap2 passed
#    Time: 25 ns Started: 15 ns  Scope: sva_ca_sequence.cap2 File: sva_ca_sequence.sv Line: 68
# ** Info: cap5 passed
#    Time: 25 ns Started: 25 ns  Scope: sva_ca_sequence.cap5 File: sva_ca_sequence.sv Line: 96
# ** Error: cap1 failed
#    Time: 25 ns Started: 15 ns  Scope: sva_ca_sequence.cap1 File: sva_ca_sequence.sv Line: 63
# ** Info: cap1 passed
#    Time: 25 ns Started: 5 ns  Scope: sva_ca_sequence.cap1 File: sva_ca_sequence.sv Line: 63
 */
